package kodkod.analysis.ordering;

import java.text.DecimalFormat;
import java.text.DecimalFormatSymbols;
import java.text.NumberFormat;
import java.util.ArrayList;

import kodkod.analysis.Analyzer;
import kodkod.analysis.OrderableSolver;
import kodkod.ast.Relation;
import kodkod.engine.fol2sat.Translation;

public class InvertedUniformPromotion extends AbstractOrdering {
	
	double weight = 1.0;
	Analyzer analyzer = null;

	public InvertedUniformPromotion() {
		this(1.0);
	}
	
	public InvertedUniformPromotion(double weight) {
		super();
		this.weight = weight;
	}
	
	public InvertedUniformPromotion(Analyzer analyzer, double weight) {
		super();
		this.weight = weight;
		this.analyzer = analyzer;
	}
	
	public void apply(Translation translation) {
		if (analyzer == null) {
			analyzer = new Analyzer(translation);
		}
		
		ArrayList<Integer> indices = analyzer.getRelationIdsOrdered();
		
		for (int pos = indices.size()-1; pos >= 0; pos--) {
			Relation rel = translation.primaryRelations.get(indices.get(pos));
			int[] vars = translation.primaryVariables(rel).toArray();
			
			for (int var : vars) {
				weightVariable((OrderableSolver)translation.cnf(), var, weight);
			}
		}
	}
	
	public String toString() {
		if (softOrder) {
			StringBuffer buf = new StringBuffer();
			buf.append("UniformInitializeInverted");
			DecimalFormatSymbols symbols = new DecimalFormatSymbols();
			symbols.setDecimalSeparator('.');
			NumberFormat format = new DecimalFormat("#0.00", symbols);
			buf.append("(");
			buf.append(format.format(weight));
			buf.append(")");
			return buf.toString();
		} else {
			return "UniformOverride";
		}
	}
}
